Maybe for some useful context: The way I’m imaging most of our usage will look like is that we’ll call an interface choice on an interface contract id. I don’t actually care much about being able to call an interface choice on a template contract id. So I think a design where we have:

1. Typechecked conversions from a template contract id to an interface contract id provided there is an implementation.
2. Typechecked exercises of interface choices on interface contract ids.
3. No exercise of interface choices on template contract ids (maybe with some fallback).

is worth considering imho.

I have a prototype interface that appears to do the right things, accepting and rejecting the proper expressions, as explained in the sample function therein.

Specifically, this makes quite a different representation of interface contract IDs from that in #11280 (and will remove mbSubst); @Robin-da do you foresee any problems regarding this in the sample linked above?

What happens if we drop that? Does that make all casts typecheck or only if you specify never explicitly as the type?

I'm not really sure. The problem with predicting this is that, as the comment mentions, a surprising number of type expressions are = to never.

All of the examples in the file work out the same if I drop the conditional. But I can then pass I3 & I2 as a type parameter to toInterface to (invalidly) convert a T contract ID to an I3 contract ID. (I3 & I2 = never.) I can also pass I1 & I2 to get an I3 contract ID, for the same reason. Are there cases where these would be inferred? Are there other surprising, perhaps more inferrable types that would = never and thus perform this coercion? I don't know.

where you don’t know the set of implemented interfaces upfront.

This will never happen, even with retroactives. We codegen on the whole environment.

Interplay with interface hierarchies

None of the codegens model these at all, only template/interface relationships.

This will never happen, even with retroactives. We codegen on the whole environment.

This is not really how daml2js works atm. Yes it has a complete environment in theory but the way it process things atm it looks at one package at a time and its dependencies not the whole package. I also don’t think it’s as simple as just looking at the whole environment:

Consider this example:

1. Package A defines template T
2. Package B defines interface I and a retroactive instance for T

Daml2js generates each LF package as a separate JS package. In this example you would thus have two JS package.
Package B can definitely depend on package A (after all it does depend on it in Daml).
With your approach you introduce a dependency from package A on package B.
So now you have a circular dependency and things go bad.

Yes it has a complete environment in theory but the way it process things atm it looks at one package at a time and its dependencies not the whole package.

We can deal with this, since we can pass extra arguments about the environment. #14082

Package B can definitely depend on package A (after all it does depend on it in Daml).

I agree this is a problem. The module dependencies end up potentially circular and breaking here.

I'd rather not add toInterface to the interfaces and have users have to know whether it was retroactive or not to know which method to call. Perhaps a function in @daml/types toInterface(TC, IC, cid) that has type overloads to either use type information in the Template Companion or the Interface Companion? (Not having typeclasses is really unfortunate.)

toInterface(TC, IC, cid) that has type overloads to either use type information in the Template Companion or the Interface Companion? (Not having typeclasses is really unfortunate.)

That sounds sensible to me. I think it’s worth thinking about whether we can use a similar design in the JVM codegens but that’s a separate conversation.

@chunlokling-da and I reworked the prototype to properly support retroactive implementations; see the new version here. Key changes:

1. Extra argument to toInterface and unsafeFromInterface, goal is to have the API be consistent for TypeScript users no matter whether the implementation is retroactive (RI4) or not
2. Conditional removed; the fact that you must pass in companion evidence makes it no longer necessary

What do you think @cocreature ?